A fundamental ability for security protocols is that of generating and communicating private \emph{nonces};
process calculi for security therefore include mechanisms for creating and communicating local names.
Neither \ntcc nor its predecessor \tcc \cite{tcc-lics94} features such mechanisms. 

As a remedy to this, in \cite{Olarte:08:SAC} we introduced the Universal Timed \ccp  process calculus (\utcc): a generalization of  
\tcc that allows for the communication of local names (or \emph{links}). 
This additional expressiveness paves the way for the declarative modeling of a wider class of systems, most notably dynamic ones.

We have endowed \utcc with a number of reasoning techniques for reachability analysis.
% we introduced the 
%\tcc\ , the deterministic version of \ntcc. %, which corresponds to  . 
%The \utcc calculus allows for the generation and communication of \emph{private nonces} as typically done for security protocols. We endowed \utcc\ with %an operational semantics and then with 
A \emph{symbolic semantics} was defined to deal with problematic operational aspects involving infinitely many substitutions which often arise when modeling security protocols.  %The novelty of the symbolic semantics is that it  
%Remarkably, this semantics 
The semantics uses temporal constraints to  finitely represent infinitely-many substitutions; it has been used 
%In \cite{Olarte:08:SAC} %Furthermore, 
%we used this semantics 
to exhibit secrecy flaws in some security protocols \cite{Olarte:08:SAC}.
%The % We also show that 
The \utcc calculus %calculus 
also  enjoys a \emph{declarative view} of processes as  First-Order Temporal Logic (FLTL) formulae \cite{mp91}. This %view 
allows for  reachability analysis of \utcc\ processes using FLTL techniques. 
For instance, in \cite{Olarte:08:SAC}  we 
%showed  that it is possible to 
used the FLTL formulae representing the model of a protocol to know if 
it  reaches  a state  where the attacker  knows a secret. 
%(i.e. if there exists a  secrecy breach. 

 We %studied the semantic foundations of \utcc\ in \cite{Olarte:08:PPDP} by 
also defined a denotational semantics for \utcc \cite{Olarte:08:PPDP}. %We showed that  
This way, processes can be represented %in this denotational semantics 
as partial closure operators. %The denotation % is %was shown to be 
%fully abstract wrt the input-output behavior of processes for a meaningful fragment of the calculus.  
As an application of the semantics, % semantic study, 
we identified a language for security protocols that can be represented as closure operators over a cryptographic constraint system.  
We showed that the least fixed point of such an operator may then be used to check a secrecy property in a protocol.  
To our knowledge, %no closure operator 
this is the first 
denotational account %has previously been given 
in the context of calculi for security protocols. 

This way, our work has brought new semantic insights into the verification of security protocols, and is related to 
%This is related to 
% It must be pointed out that there are several instances of 
the research in security protocols %that have used tools and techniques 
from areas closely related to \ccp. Namely, Constraint Programming (e.g. \cite{BellaB04}) and Logic Programming (e.g. \cite{AbadiBlanchetJACM7037,millen95}). 
To our  knowledge there is no work on Security Protocols that takes advantage of the reasoning techniques of \ccp.  

%\subsubsection{Related Results}
%We studied the expressiveness of \utcc\ in \cite{Olarte:08:PPDP}. We showed that in contrast to \tcc, \utcc\ is Turing-powerful by encoding Minsky machines. The encoding used a monadic constraint system allowing us to prove a new result for a fragment of first-order linear-rime temporal logic (FLTL): The undecidability of the validity problem for monadic FLTL without equality and function symbols. This result refuted a decidability conjecture for FLTL from a previous paper. It also justified the restriction imposed in previous decidability results on the quantification of flexible-variables. 

